COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR x x0 x1 x2 y y0 y1 y2 z z0 z1 z2 ε block
C00004 00003	axiom tower:
C00005 ENDMK
C⊗;
declare INDVAR x x0 x1 x2 y y0 y1 y2 z z0 z1 z2 ε block;
declare INDVAR tower tower1 tower2 t t0 t1 t2 ε tower;
declare INDCONST A B C D Table ε block;

declare INDVAR s s0 s1 s2 ε situation;
declare INDCONST S0 ε situation;

declare PREDCONST on(block,block,situation);
declare PREDCONST above(block,block,situation);
declare PREDCONST clear(block,situation);
declare PREDCONST reachable(situation,situation) [inf];

declare OPCONST move(block,block,situation) = situation;

axiom above:
	∀x y s.(on(x,y,s) ⊃ above(x,y,s))
	∀x s.¬above(x,x,s)
	∀x y z s.(above(x,y,s) ∧ above(y,z,s) ⊃ above(x,z,s))
;;

axiom move:
	∀x y s.(clear(x,s) ∧ (clear(y,s) ∨ y = Table) ∧ ¬(x = y) ⊃
		∀y1.(on(x,y1,move(x,y,s)) ≡ y1 = y) ∧
		∀z1 z2.(¬(z1 = x) ⊃ (on(z1,z2,move(x,y,s)) ≡ on(z1,z2,s))))
	∀x y s.(¬clear(x,s) ∨ (¬clear(y,s) ∧ ¬(y = Table)) ⊃
		∀s1.¬(move(x,y,s) = s1))
;;

axiom distinct:
	¬(A=B ∨ A=C ∨ A=D ∨ A=Table ∨ B=C ∨ B=D ∨ B=Table ∨ C=D ∨ C=Table ∨
		D=Table)
;;

axiom clear:
	∀x s.(clear(x,s) ≡ ∀y.¬on(y,x,s))
;;

axiom unique:
	∀x1 x2 y s.(¬(y=Table) ∧ on(x1,y,s) ∧ on(x2,y,s) ⊃ x1 = x2)
;;

axiom reachable:
	∀x y s.(reachable(s,move(x,y,s))
;;
axiom tower:
	∀t1 t2 t2.(t1 over (t2 over t3) = (t1 over t2) over t3)
;;